tla/ChotkiSync.tla models the replication protocol end to end: the
Syncer feed/drain state machines, pebble-snapshot diff sync with
sync-point batches applied on 'V', broadcast relaying over a replica
tree, and network read batching (record coalescing). TLC configs check
the fixed protocol (NoGaps, exact/complete block VVs, one diff sync per
src, quiescent convergence - all pass, see tla/README.md) and reproduce
three real protocol bugs as counterexamples:

1. Drain() did not rebroadcast a batch whose last record was 'B' (bye),
   nor the applied prefix of a batch failing mid-way. Records applied at
   the middle replica never reached downstream ones, and the next
   re-handshake merged the origin's version vector downstream without
   the data, making the loss permanent and silent. Drain now relays
   exactly the locally-applied prefix minus the session-scoped trailing
   'B' (Chotki.DrainApplied + Syncer.relayApplied).

2. The "allow only 1 diff sync per src" cleanup in drain() 'H' compared
   sync-point keys against cho.src, which never matches since a replica
   never drains its own handshake; stale sync points were never
   displaced. It now compares against the incoming handshake's source.

3. (found by TLC) A sync point outlived the session whose relayed 'H'
   created it: when a downstream link reconnected mid-relay, the relayed
   'D' records died with the old connection while the relayed 'V'
   arrived over the new one and applied the staged handshake VV without
   the data - permanent silent data loss on any network blip during a
   relayed diff sync. Sync points are now bound to the session that
   created them (Syncer.SessionId carried in the drain context) and
   aborted when it closes (Chotki.AbortSyncsVia).

Also fixed along the way (details in tla/README.md):
- draining a peer's bye no longer cuts our own diff short of its 'V'
  (the peer would silently miss the promised data; TestChotki_Sync3
  flaked on this)
- Syncer.Close raced concurrent Feed over the pebble snapshot iterators
  (mergingIter panic under -race); guarded by snapLock
- Feed's SendNone wait could block forever when a late Drain moved the
  drain state backwards after the one-shot unblock timer had fired
- WaitDrainState leaked two goroutines per call; processPings skipped
  the record following a removed ping; Feed's SendPing case mutated
  pingTimer without the lock
- ApplyD/ApplyV looped forever on truncated inner TLV records; ApplyV
  overwrote earlier errors; ApplyH merged a nil VV from a malformed
  relayed handshake; drain() 'H' registered the sync point even when
  ApplyH failed
- test fixes: examples left a DB open racing its cleanup; index tests
  waited only 5s for the background reindex worker